1. Technical Field
An “Automated, Static Safety Verifier”, as described herein, uses typed assembly language (TAL) and Hoare logic to achieve highly automated, static verification of both type and memory safety for constructing a “safe” operating system.
2. Related Art
Low-level software, such as operating systems and language run-time systems, should be reliable and secure. Without reliability, users endure frustration and potential data loss when the system software crashes. Without security, users are vulnerable to attacks from the network, which often exploit low-level bugs such as buffer overflows to take over a user's computer. Unfortunately, today's low-level software still suffers from a steady stream of bugs, often leaving computers vulnerable to attack until the bugs are patched.
Many projects have proposed using safe languages to increase the reliability and security of low-level systems. Safe languages ensure type safety and memory safety: accesses to data are guaranteed well-typed and guaranteed not to overflow memory boundaries or dereference dangling pointers. This safety rules out many common bugs, such as buffer overflow vulnerabilities. Unfortunately, even if a language is safe, implementations of the language's run-time system might have bugs that undermine the safety. For example, such bugs have left many conventional web browsers open to attack.
The desire to formally verify low-level operating systems (OS) and run-time system code is not new. Nevertheless, very little mechanically verified low-level OS and run-time system code exists, and, as is known to those skilled in the art, that code still requires many person-years of effort to verify.
For example, with respect to OS and run-time system verification efforts, more than 20 years ago, the well-known Boyer-Moore mechanical theorem prover verified a small OS and a small high-level language implementation. These were not integrated into a single system, though, and each piece in isolation was quite limited. The OS, referred to as “Kit”, was quite small, containing just a few hundred assembly language instructions. It supported a fixed number of preemptive threads, but did not implement dynamic memory allocation or thread allocation. Further, it ran on an artificial machine rather than on standard hardware. The language used, “micro-Gypsy”, was small enough that it did not require a significant run-time system, as it had no heap allocation or threads.
More recently, the well-known “seL4” project verified all of the C code for an entire microkernel. seL4 works on uni-processors, providing preemption via interrupts, and providing non-blocking system calls. seL4 also provides memory protection by providing address spaces of pages protected by hardware page tables. Unfortunately, seL4 does not provide objects that are protected by type safety. Further, seL4 processes communicate through shared memory or message passing. Therefore, unfortunately, seL4 does not have a communication mechanism that is statically checked for safety. In addition, seL4 verifies its C code; however, its assembly language (˜600 lines of ARM assembler) is currently unverified. The seL4 microkernel contained ˜8700 lines of C code, substantially larger than earlier verified operating systems like Kit. On the other hand, the effort required was also large. In fact, it was reported that the seL4 project required 20 person-years of research devoted to developing their proofs, including 11 person-years specifically for the seL4 code base. The proof required 200,000 lines of Isabelle scripts—a 20-to-1 script-to-code ratio. Thus, while seL4 demonstrates that microkernels are within the reach of interactive theorem proving, the seL4 project fails to provide an acceptably efficient solution to the problem of realistic systems software verification.
The well-known “FLINT” project sets an ambitious goal to build foundational certified machine code, where certification produces a proof about an executable program, and a very small proof checker can verify the proof. The FLINT project uses powerful higher-order logic to verify properties of low-level code, but fails to achieve significant automation. For example, the preemptive thread library of the FLINT project requires ˜35,000 lines of script for about 300 lines of assembly language (plus many tens of thousands of lines of script to build up foundational lemmas about the program logic). Separately, the FLINT project also created a certified system combining TAL with certified garbage collection (GC). Unfortunately, the TAL/GC system was rather limited in that it supported only objects containing exactly two words. Further, it performed only conservative collection, and did not support multiple threads.
Finally, as is well-known to those skilled in the art, H monads have been used to export a set of operating system primitives usable to develop an operating system in a high-level language. For example, H was used to build the well-known “House” operating system. However, H itself is not formally verified, and relies on a large Haskell run-time system for correctness.